\begin{tabbing}
(\=(Unfolds ``all exists`` 4) \+
\\[0ex]CollapseTHEN (RenameVar `g' 4))$\cdot$
\-
\end{tabbing}